\documentclass{article}
\usepackage{url}
\usepackage{manfnt}
\usepackage{fullpage}
\usepackage{proof}
\usepackage{amssymb}
\usepackage{latexsym}
\usepackage{xcolor}
\usepackage{mathrsfs}
\usepackage{amsmath, amsthm}
\usepackage{stmaryrd}

\newcommand{\frank}[1]{\textcolor{blue}{\textbf{[#1 --Frank]}}}
% My own macros
\newcommand{\m}[2]{ \{\mu_{#1}\}_{#1 \in #2}} 
\newcommand{\M}[3]{\{#1_i \mapsto #2_i\}_{i \in #3}} 
\newcommand{\fmu}[0]{ \mathbf{F}_{\omega}^{\mu}} 
\newcommand{\bred}[0]{\to_{\beta}} 
\newcommand{\rat}[0]{\rightarrowtail} 
\newcommand{\polym}[1]{\rightarrowtail_{#1}} 
\newcommand{\tyred}[0]{\to_{\tau}} 
\newcommand{\interp}[1]{\llbracket #1 \rrbracket} 

\newcommand{\inn}{\downarrow} 
\newcommand{\out}{\uparrow} 

\newtheorem{prop}{Proposition}
\newtheorem{definition}{Definition}
\newtheorem{corollary}{Corollary}
\newtheorem{lemma}{Lemma}
\newtheorem{theorem}{Theorem}

 
\begin{document}
%\pagestyle{empty}
\title{$\mathbf{FK}_{\mu} \to \mathbf{FK}$}
\author{ 
Computer Science, The University of Iowa}
\date{\today}


\maketitle
\thispagestyle{empty}

\section{System $\mathbf{FK}$}

\begin{definition}[Syntax]

\

\noindent \textit{Terms} $t \ :: = \ x \ | \ \lambda x.t \ | \ t t'$

\noindent \textit{Types} $T \ ::= \ X \ | \ F \vec{T} \ | \ \Pi X.T \ | \ T_1 \to T_2$

\noindent \textit{Funktor} $F \ ::= \lambda \vec{X}.T$ 

\noindent \textit{Context} $\Gamma \ :: = \ \cdot \ | \ \Gamma, x:T$ 

\end{definition}

\begin{definition}[Typing Rules]
\


\begin{tabular}{lll}
    
\infer[\textit{Var}]{\Gamma \vdash x:T}{(x:T) \in \Gamma}

&

\infer[\textit{Conv}]{\Gamma \vdash t : T_2}{\Gamma \vdash t:
T_1 & \Gamma \vdash T_1 = T_2}

\\
\\
\infer[\textit{Intro}]{\Gamma \vdash \lambda x.t :T_1 \to T_2}
{\Gamma, x:T_1 \vdash t: T_2}

&

\infer[\textit{Elim}]{\Gamma \vdash t t':T_2}{\Gamma
\vdash t:T_1 \to T_2 & \Gamma \vdash t': T_1}

\\
\\

\infer[\textit{Gen}]{\Gamma \vdash t :\Pi X.T}
{\Gamma \vdash t: T & X \notin \mathrm{FV}(\Gamma)}

&
\infer[\textit{Inst}]{\Gamma \vdash t:[T'/X]T}{\Gamma \vdash t: \Pi X.T}
\end{tabular}

\end{definition}

\begin{definition}[Funktorial Conversion]
  $(\lambda \vec{X}.T) \vec{T'} = [\vec{T'}/\vec{X}]T$
\end{definition}

\begin{definition}[Lambda Conversion]
  $(\lambda x.t) t' = [t'/x]t$
\end{definition}

\section{$\mathbf{FK}_{\mu}$ }

\begin{definition}
  \
  
\noindent \textit{Terms} $t \ :: = \ x \ | \ \lambda x.t \ | \ t t'\ | \ \inn t\ | \ \out t $

\noindent \textit{Types} $T \ ::= \ X \ | \ F T\ | \ \Pi X.T \ | \ T_1 \to T_2 \ |\ \mu X. \mathbf{1} + T \times X$

\noindent \textit{Funktor} $F \ ::= \lambda \vec{X}.T$ 

\noindent \textit{Context} $\Gamma \ :: = \ \cdot \ | \ \Gamma, x:T$ 

\end{definition}


\begin{definition}[Typing Rules]
\


\begin{tabular}{lll}
    
\infer[\textit{Var}]{\Gamma \vdash x:T}{(x:T) \in \Gamma}

&

\infer[\textit{Conv}]{\Gamma \vdash t : T_2}{\Gamma \vdash t:
T_1 & \Gamma \vdash T_1 = T_2}

\\
\\
\infer[\textit{Intro}]{\Gamma \vdash \lambda x.t :T_1 \to T_2}
{\Gamma, x:T_1 \vdash t: T_2}

&

\infer[\textit{Elim}]{\Gamma \vdash t t':T_2}{\Gamma
\vdash t:T_1 \to T_2 & \Gamma \vdash t': T_1}

\\
\\

\infer[\textit{Gen}]{\Gamma \vdash t :\Pi X.T}
{\Gamma \vdash t: T & X \notin \mathrm{FV}(\Gamma)}

&
\infer[\textit{Inst}]{\Gamma \vdash t:[T'/X]T}{\Gamma \vdash t: \Pi X.T}
\\
\\

\infer[\textit{in}]{\Gamma \vdash \inn t : \mu X. \mathbf{1} + T \times X}
{\Gamma \vdash t: \mathbf{1} + T \times (\mu X. \mathbf{1} + T \times X)}

&

\infer[\textit{out}]{\Gamma \vdash \out t : \mathbf{1} + T \times (\mu X. \mathbf{1} + T \times X)}
{\Gamma \vdash t: \mu X. \mathbf{1} + T \times X}


\end{tabular}

\end{definition}

\begin{definition}[Funktorial Conversion]
  $(\lambda X.T) T' = [T'/X]T$
\end{definition}

\begin{definition}[Conversion]
  $(\lambda x.t) t' = [t'/x]t$ and $\out \inn t = t$
\end{definition}

\noindent \textbf{Conventions:}
\begin{itemize}
\item We require $\mu \notin T$ for $\mu X. \mathbf{1} + T \times X$. 
\item $\mathbf{1}$ stands for the type $\Pi X.X \to X$ with inhabitant $\lambda x.x$. 
\item $+ := \lambda (U,V). \Pi X.(U \to X) \to (V \to X) \to X$.
  
\item $\iota_1 := \lambda u.\lambda x.\lambda y.x u$ and $\iota_2 := \lambda u.\lambda x.\lambda y.y u$.
\item $\delta :=  \lambda y.\lambda z. \lambda t.t y z$, usually we use it by $\delta  (\lambda x.u) (\lambda y.v) \ t$. 
\item Reduction $\delta (\lambda x.u) (\lambda y.v) (\iota_1 r) \to^* [r/x]u$ and $\delta (\lambda x.u) (\lambda y.v) (\iota_2 r) \to^* [r/y]v$

\item $\times := \lambda (U,V). \Pi X.(U \to V \to X) \to X$. 
\item $(\ ,\ ) := \lambda u.\lambda v.\lambda x.x u v$ and $\pi_1 := \lambda t.t (\lambda x.\lambda y.x)$, $\pi_2 := \lambda t.t (\lambda x.\lambda y.y)$.
\item $\pi_1 (u,v) \to^* u$ and $\pi_2 (u,v) \to^* v$.
\end{itemize}
\section{Reduction}
\begin{definition}
  \
  
  $G(\mu X. \mathbf{1} + T \times X ) := \Pi X.(\mathbf{1} + T \times X \to X) \to X$.
  
  $G(X) := X$
  
  $G(\Pi X.T) := G(T)$
  
  $G(T \to T') := G(T) \to G(T')$
  
  $G(F T) := G(F) \to G(T)$
  
  $G(\lambda X.T):= \lambda X.G(T)$
\end{definition}

\begin{definition}[Wadler's Fold in $\mathbf{FK}$]
  \
  
  $\phi: \Pi X.(\mathbf{1} + T \times X \to X) \to (\Pi Y.(\mathbf{1} + T \times Y \to Y) \to Y) \to X$
  
  $\phi := \lambda k[:\mathbf{1} + T \times X \to X].\lambda t[: \Pi Y.(\mathbf{1} + T \times Y \to Y) \to Y]. t k$
\end{definition}

\begin{definition}[Wadler's Functor in $\mathbf{FK}$]
  \
  
  $\tau :\Pi X.\Pi Y. (X \to Y) \to (\mathbf{1} + T \times X \to \mathbf{1} + T \times Y)$
  
  $\tau := \lambda f[: X \to Y]. \delta (\lambda x[:\mathbf{1}]. \iota_1 x) (\lambda y[:T \times X]. \iota_2 (\pi_1 y, f (\pi_2 y))) $

  
\end{definition}
\noindent Note that $\delta (\lambda x[:\mathbf{1}]. \iota_1 x) (\lambda y[:T \times X]. \iota_2 (\pi_1 y, f (\pi_2 y))) \to_{\beta} $

\noindent $\lambda t[: \mathbf{1}+T\times X]. t (\lambda x[:\mathbf{1}]. \iota_1 x) (\lambda y[:T \times X]. \iota_2 (\pi_1 y, f (\pi_2 y)))$. 

\noindent So $\delta (\lambda x[:\mathbf{1}]. \iota_1 x) (\lambda y[:T \times X]. \iota_2 (\pi_1 y, f (\pi_2 y))) : \mathbf{1} + T \times X \to \mathbf{1} + T \times Y$. 

\begin{definition}[In in $\mathbf{FK}$]
\

$\inn : (\mathbf{1}+ T \times (\Pi X.(\mathbf{1} + T \times X \to X) \to X))\to (\Pi X.(\mathbf{1} + T \times X \to X) \to X) $ 

$\inn := \lambda s[:\mathbf{1}+ T \times (\Pi X.(\mathbf{1} + T \times X \to X) \to X)]. \lambda k[:\mathbf{1}+ T\times X \to X]. k (\tau (\phi k) s)$
\end{definition}


\begin{definition}[Out in $\mathbf{FK}$]
\

$\out :   (\Pi X.(\mathbf{1} + T \times X \to X) \to X) \to (\mathbf{1}+ T \times (\Pi X.(\mathbf{1} + T \times X \to X) \to X))$
  
$\out := \phi [\mathbf{1}+ T \times (\Pi X.(\mathbf{1} + T \times X \to X) \to X)] (\tau \inn)$  
\end{definition}

\begin{theorem}[Meta]
For any $\cdot \vdash t: \mathbf{1} + T \times (\mu X. \mathbf{1} + T \times X)$, $\out \inn t \to_{\beta} t$. \frank{Need canonical form to prove this. This is similar to the product behavior in System \textbf{F}. Now things become tricky.}
\end{theorem}
\begin{theorem}
If $\Gamma \vdash t:T$ in $\mathbf{FK}_{\mu}$, then $G(\Gamma) \vdash t:G(T)$ in $\mathbf{FK}$.   
\end{theorem}


\end{document}
